$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$, ${\it e'}$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} .
\\[0ex](lastchange($x$;$e$) = lastchange($x$;${\it e'}$) $\in$ E) $\Rightarrow$ $\forall$${\it e''}$$\in$[${\it e'}$,$e$).($x$ after ${\it e''}$) = ($x$ when $e$) $\in$ $T$